Newman's lemma
In the theory of rewriting systems, Newman's lemma states that a terminating (or strongly normalizing) abstract rewriting system (ARS), that is, one in which there are no infinite reduction sequences, is confluent if it is locally confluent. In fact a terminating ARS it is confluent precisely when it is locally confluent.
Today, this is seen as a purely combinatorial result based on well-foundedness due to a proof of Gérard Huet in 1980. Newman's original proof was considerably more complicated.[1]
An earlier proof of the theorem was given by Church and Rosser.
Notes
- ^ Harrison, p. 260, Paterson(1990), p. 354.
References
- M. H. A. Newman. On theories with a combinatorial definition of "equivalence". Annals of Mathematics, 43, Number 2, pages 223--243, 1942.
- Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), October 1980, Volume 27, Issue 4, pp. 797 - 821.
- Paterson, Michael S. (1990). Automata, languages, and programming: 17th international colloquium. Lecture notes in computer science. 443. Warwick University, England: Springer. ISBN 9783540528265.
- A. Church and J. B. Rosser, Some properties of conversion, Transactions of the American Mathematical Society, 39(3), 1936.
Textbooks
- Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003. (book weblink)
- Term Rewriting and All That, Franz Baader and Tobias Nipkow, Cambridge University Press, 1998 (book weblink)
- John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009, ISBN 9780521899574, chapter 4 "Equality".
External links